Lambda the Ultimate

The Derivative of a Regular Type is its Type of One-Hole Contexts by Conor McBride was mentioned on LtU several times.

If you enjoyed it, try a new paper by the same author:
Clowns to the left of me, jokers to the right (Dissecting Data Structures).

More generic programming, more parallels between data types and calculus, more fun.

As usual for Conor's paper, it's short and full of (sometimes obscure) humor. Beware of typos, though.

EWD831 by E.W. Dijkstra, 1982.

When dealing with a sequence of length N, the elements of which we wish to distinguish by subscript, the next vexing question is what subscript value to assign to its starting element. Adhering to convention a) yields, when starting with subscript 1, the subscript range 1 ≤ i < N+1; starting with 0, however, gives the nicer range 0 ≤ i < N. So let us let our ordinals start at zero: an element's ordinal (subscript) equals the number of elements preceding it in the sequence. And the moral of the story is that we had better regard —after all those centuries!— zero as a most natural number.

Remark Many programming languages have been designed without due attention to this detail. In FORTRAN subscripts always start at 1; in ALGOL 60 and in PASCAL, convention c) has been adopted; the more recent SASL has fallen back on the FORTRAN convention: a sequence in SASL is at the same time a function on the positive integers. Pity! (End of Remark.)

What's the modern trend for indexing from zero vs. indexing from one? And for specifying ranges ("from 5 to 8", 5 ≤ N < 9, "four elements starting from 5")? Why?

Several interesting papers have been published by researchers at the University of Colorado investigating ways of making end-user programming more accessible, especially to secondary-level (i.e., High School) students. In many ways, this work reminds me of the efforts of the PLT group and their excellent DrScheme software implementation, though its strong graphical leanings makes for wonderful eye candy.

I stumbled across this body of work while trying to generate some OpenGL models from Common Lisp. It turns out that most of the AgentSheets system is built on top of a DSL embedded in Common Lisp called AgenTalk. AgentTalk is implemented on top of MCL and Allegro Common Lisp. (Interestingly, an apparently independent AgentTalk appears to have been implemented on top of DrScheme.)

I found several items of note:

1. Discussion of AntiObjects as a way of designing large systems (as a foil to the Booch system.)
2. Descriptions of compelling 3-D authoring environments for non-technical users.
3. Some neat old-school Macintosh examples from the early days of AgentSheets.
4. A wonderful 3D Lisp Programming Library, the Open Agent Engine, which is used to power all of the above examples.

An interesting blog post from Ralf Lammel which may raise some reactions...

The post refers to the paper JavaGI: Generalized Interfaces for Java (Stefan Wehr and Ralf Lammel and Peter Thiemann). Here's a teaser:

generalized interfaces cater for retroactive and conditional interface implementations, binary methods, static methods, default methods, interfaces over families of types, and existential quantification for interface-bounded types. As a result, many anticipatory uses of design patterns such as Adapter, Factory and Visitor become obsolete...

I just heard about Papert's tragic accident. Thankfully, what I am reading suggests that his condition is improving.

Papert is the father of the Logo programming language which, apart from being the first programming language I learned, is one of the most important attempts to use computers, and programming in particular, in education.

Flowers for Seymour is an attempt to create a virutal flower album to provide emotional support for Papert and his family. This is a nice gesture, and I hope the LtU community will contribute to it. The album includes only a few flower images created in Logo, which is a shame. It would be nice to see more images created using the wonderful tool Papert gave us.

Our prayers are with Seymour Papert and his family.

Data Parallel Haskell: a status report. Manuel M. T. Chakravarty, Roman Leshchinskiy, Simon Peyton Jones, Gabriele Keller, and Simon Marlow.

We describe the design and current status of our effort to implement the programming model of nested data parallelism into the Glasgow Haskell Compiler. We extended the programming model and its implementation, both of which were first popularised by the NESL language, in terms of expressiveness as well as efficiency of its implementation. Our current aim is to provide a convenient programming environment for SMP parallelism, and especially multicore architectures. Preliminary benchmarks show that we are, at least for some programs, able to achieve good absolute performance and excellent speedups.

NESL was mentioned here in the past a few times, as was data parallelism in general.

This will be of interest to LtU readers in India and maybe for others as well.

The Joins Concurrency Library. Claudio Russo.

Comega extended C# 1.x with a simple, declarative and powerful model of concurrency - join patterns - applicable both to multithreaded applications and to the orchestration of asynchronous, event-based distributed applications. With Generics available in C# 2.0, we can now provide join patterns as a library rather than a language feature. The Joins library extends its clients with an embedded, type-safe and mostly declarative language for expressing synchronization patterns. The library has some advantages over Comega: it is language neutral, supporting other languages like Visual Basic; its join patterns are more dynamic, allowing solutions difficult to express with Comega; its code is easy to modify, fostering experimentation.

In the Joins library, the scheduling logic that would be compiled into the corresponding Comega class receives a separate, first-class representation as an object of the special Join class. The Join class provides a mostly declarative, type-safe mechanism for defining thread-safe synchronous and synchronous communication channels and patterns. Instead of (a)synchronous methods, as in Comega, the communication channels are special delegate values (first-class methods) obtained from a common Join object. Communication and/or synchronization takes place by invoking these delegates, passing arguments and optionally waiting
for return values.

The library also supports dynamic joins, which are not available in Comega, implemented by joining arrays of channels (with the size of the array being determined at runtime).

The major weakness of the Joins library is speed, since the static apporach of Comega provides more room for optimization (see the brief discussion in sec. 6).

A recent enlightening discussion on recursive type inference at comp.lang.functional brought the following tutorial paper on ML type inference to my attention.

A modern eye on ML Type Inference by Francois Pottier INRIA September 2005.

Hindley and Milner’s type system is at the heart of programming languages such as Standard ML, Objective Caml, and Haskell. Its expressive power, as well the existence of a type inference algorithm, have made it quite successful. Traditional presentations of this algorithm, such as Milner’s Algorithm W, are somewhat obscure. These short lecture notes, written for the APPSEM’05 summer school, begin with a presentation of a more modern, constraint-based specification of the algorithm, and explain how it can be extended to accommodate features such as algebraic data types, recursion, and (lexically scoped) type annotations. Then, two chapters, yet to be written, review two recent proposals for incorporating more advanced features, known as arbitrary-rank predicative polymorphism and generalized algebraic data types. These proposals combine a traditional constraint-based type inference algorithm with a measure of local type inference.

Classical versus Quantum Computation. John Baez.

This fall, John Baez has been conducting a seminar on classical and quantum computation. So far they appear to have covered mostly foundations of classical computation (lambda calculus, CCCs, the fixed point theorem). It's interesting to see lambda calculus introduced to an audience already comfortable with category theory.

Excellent lecture notes are available for each week with a bit of supporting material, and there have been blog posts for each class on The n-Category Cafe (the most recent one is here). The blog posts have some extra discussion, and comments, of course.

The seminar continues in the spring and I'm sure people may want to follow along...